#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"

int foo(int a, int b) {
	int c=0;
	if(klee_change(0,1)){
		for (int i=1;i<=b;++i)
		    c-=a;
	}
	else{
		for (int i=1;i<=a;++i)
		    c+=b;
	}
	return c;
}

int main(int argc, char *argv[]) {
    int x = (argv[1][0] - '0') * 10 + (argv[1][1] - '0');
    if (x>=18 && x<22)
	    return foo(x,20);
    return 0;
}
